Nuprl Lemma : es-time-sender 11,40
es:event_system{i:l}, e:es-E(es).
(es-isrcv(es; e))  qle(es-time(es; es-sender(es; e)); es-time(es; e)) 
latex

Definitionst  T, P  Q, x:A. B(x), prop{i:l}
Lemmasevent system wf, es-E wf, es-isrcv wf, assert wf, es-sender-causl, es-sender wf, es-time-order

origin